Example 1 in [Giesl and Middeldorp - DLT'02]

Summary: Ex1_GM03

• CS-TRS format
• OBJ format
• Negative results:
  1. CSRPO
  2. Lucas' transformation (Extra variables)
• Positive results:
  1. (Innermost) Giesl and Middeldorp's transformation
  2. Giesl and Middeldorp's tranformation (Corollary)

CS-TRS Ex1_GM03 (file Ex1_GM03.csr)

Functions:  p 0 s leq true false if diff

Constructors:  0 s true false

Variables:  X Y

Arities: 

ar(p) = 1
ar(0) = 0
ar(s) = 1
ar(leq) = 2
ar(true) = 0
ar(false) = 0
ar(if) = 3
ar(diff) = 2

Replacement map: 

µ(p)={1}
µ(0)={}
µ(s)={1}
µ(leq)={1,2}
µ(true)={}
µ(false)={}
µ(if)={1}
µ(diff)={1,2}

Rules:  (file Ex1_GM03)  

p(0) -> 0
p(s(X)) -> X
leq(0,Y) -> true
leq(s(X),0) -> false
leq(s(X),s(Y)) -> leq(X,Y)
if(true,X,Y) -> X
if(false,X,Y) -> Y
diff(X,Y) -> if(leq(X,Y),0,s(diff(p(X),Y)))

The CS-TRS in OBJ format (file Ex1_GM03.obj):

obj Ex1_GM03 is
  sort S .
  op p : S -> S .
  op 0 : -> S .
  op s : S -> S .
  op leq : S S -> S .
  op true : -> S .
  op false : -> S .
  op if : S S S -> S [strat (1 0)] .
  op diff : S S -> S .
  vars X Y : S .
  eq p(0) = 0 .
  eq p(s(X)) = X .
  eq leq(0,Y) = true .
  eq leq(s(X),0) = false .
  eq leq(s(X),s(Y)) = leq(X,Y) .
  eq if(true,X,Y) = X .
  eq if(false,X,Y) = Y .
  eq diff(X,Y) = if(leq(X,Y),0,s(diff(p(X),Y))) .
endo

Negative results

1. The CS-TRS Ex1_GM03 TRS is not simply µ-terminating:

          diff(s(0),0) \-> if(leq(s(0),0),0,s(diff(p(s(0)),0)))
   	  \-> if(false,0,s(diff(p(s(0)),0)))
   	  \-> s(diff(p(s(0)),0))
   	  \->_Embµ(F) diff(p(s(0)),0)
   	  \->_Embµ(F) diff(s(0),0)
   	  \-> ...
       

   Therefore, by [GL02b, Theorem 9] R cannot be proved mu-terminating by using CSRPO.
2. The µ-termination of Ex1_GM03 cannot be proved by using Lucas' transformation. The TRS Ex1_GM03_L:

       p(0) -> 0
       p(s(X)) -> X
       leq(0,Y) -> true
       leq(s(X),0) -> false
       leq(s(X),s(Y)) -> leq(X,Y)
       if(true) -> X
       if(false) -> Y
       diff(X,Y) -> if(leq(X,Y))
       

   contains extra variables.

Positive results

1. The µ-termination of Ex1_GM03 is proved by using the transformation in [GM03]. The TRS Ex1_GM03_iGM:

      active(p(0)) -> mark(0)
      active(p(s(X))) -> mark(X)
      active(leq(0,Y)) -> mark(true)
      active(leq(s(X),0)) -> mark(false)
      active(leq(s(X),s(Y))) -> mark(leq(X,Y))
      active(if(true,X,Y)) -> mark(X)
      active(if(false,X,Y)) -> mark(Y)
      active(diff(X,Y)) -> mark(if(leq(X,Y),0,s(diff(p(X),Y))))
      mark(p(X)) -> active(p(mark(X)))
      mark(0) -> active(0)
      mark(s(X)) -> active(s(mark(X)))
      mark(leq(X1,X2)) -> active(leq(mark(X1),mark(X2)))
      mark(true) -> active(true)
      mark(false) -> active(false)
      mark(if(X1,X2,X3)) -> active(if(mark(X1),X2,X3))
      mark(diff(X1,X2)) -> active(diff(mark(X1),mark(X2)))
      p(mark(X)) -> p(X)
      p(active(X)) -> p(X)
      s(mark(X)) -> s(X)
      s(active(X)) -> s(X)
      leq(mark(X1),X2) -> leq(X1,X2)
      leq(X1,mark(X2)) -> leq(X1,X2)
      leq(active(X1),X2) -> leq(X1,X2)
      leq(X1,active(X2)) -> leq(X1,X2)
      if(mark(X1),X2,X3) -> if(X1,X2,X3)
      if(X1,mark(X2),X3) -> if(X1,X2,X3)
      if(X1,X2,mark(X3)) -> if(X1,X2,X3)
      if(active(X1),X2,X3) -> if(X1,X2,X3)
      if(X1,active(X2),X3) -> if(X1,X2,X3)
      if(X1,X2,active(X3)) -> if(X1,X2,X3)
      diff(mark(X1),X2) -> diff(X1,X2)
      diff(X1,mark(X2)) -> diff(X1,X2)
      diff(active(X1),X2) -> diff(X1,X2)
      diff(X1,active(X2)) -> diff(X1,X2)
      

   can be proved innermost terminating by using the dependency pairs technique (see [GM02, Appendix A.2]). Then, Ex1_GM03 is innermost µ-terminating. Since Ex1_GM03 is orthogonal, by [GM03, Theorem 9], Ex1_GM03 is also µ-terminating.
2. By [Luc02b, Theorem 6] and [GM04, Theorem 48], the µ-termination of Ex1_GM03 can be proved by using Giesl and Middeldorp's transformation.